Nuprl Lemma : mod_bounds 13,42

a:n:. (0  (a mod n)) & ((a mod n) < n
latex


Upint 2, int 2
Definitionst  T, P & Q, x:AB(x), a mod n, T, P  Q, P  Q, P  Q, True, ff, if b then t else f fi , , tt, , False, A, a  b  T , i  j , Unit, , , A  B,
Lemmasnat plus wf, modulus wf, le wf, nat properties, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, assert wf, bool wf, le int wf, rem bounds 1, not functionality wrt iff, assert of bnot, assert of eq int, not wf, eq int wf, add cancel in lt

origin